$\forall$$A$:Type, ${\it eq}$:EqDecider($A$), $B$:($A$$\rightarrow$Type), $P$:($x$:$A$$\rightarrow$$B$($x$)$\rightarrow$Prop), $x$:$A$, $v$:$B$($x$).
\\[0ex]$\forall$$y$$\in$dom($x$ : $v$). $w$=$x$ : $v$($y$) $\Rightarrow$  $P$($y$,$w$) $\Leftrightarrow$ $P$($x$,$v$)